Compilers transform programs from high-level programming languages to machine code by a series of steps. At each stage in compilation, an intermediate language can be defined to represent programs at that stage. At each new stage, the corresponding intermediate language representation exposes more details of the computation than the previous stage up to the point where machine code is reached.
In general, a typed programming language means that its data types (e.g., integers, floats and so forth) have certain restrictions on their usage. Type checking with respect to compilers refers to ensuring at compile time that these restrictions are not violated. Typed intermediate languages thus allow intermediate program representations to be type checked, that is, that the output of a compiler provides a program that is safe to run, and thus typed intermediate languages are used to build more reliable and secure systems.
However, prior implementations of typed intermediate languages in compilers for object-oriented languages do not handle low-level implementation details such as virtual method tables, or do not model standard compilation techniques. Further, none of the prior systems have been shown to scale to compile large programs.